↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
rem_in(X, Y, X) → U4(X, Y, notZero_in(Y))
notZero_in(s(X)) → notZero_out(s(X))
U4(X, Y, notZero_out(Y)) → U5(X, Y, geq_in(X, Y))
geq_in(X, 0) → geq_out(X, 0)
geq_in(s(X), s(Y)) → U7(X, Y, geq_in(X, Y))
U7(X, Y, geq_out(X, Y)) → geq_out(s(X), s(Y))
U5(X, Y, geq_out(X, Y)) → rem_out(X, Y, X)
rem_in(X, Y, R) → U1(X, Y, R, notZero_in(Y))
U1(X, Y, R, notZero_out(Y)) → U2(X, Y, R, sub_in(X, Y, Z))
sub_in(X, 0, X) → sub_out(X, 0, X)
sub_in(s(X), s(Y), Z) → U6(X, Y, Z, sub_in(X, Y, Z))
U6(X, Y, Z, sub_out(X, Y, Z)) → sub_out(s(X), s(Y), Z)
U2(X, Y, R, sub_out(X, Y, Z)) → U3(X, Y, R, rem_in(Z, Y, R))
U3(X, Y, R, rem_out(Z, Y, R)) → rem_out(X, Y, R)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PrologToPiTRSProof
rem_in(X, Y, X) → U4(X, Y, notZero_in(Y))
notZero_in(s(X)) → notZero_out(s(X))
U4(X, Y, notZero_out(Y)) → U5(X, Y, geq_in(X, Y))
geq_in(X, 0) → geq_out(X, 0)
geq_in(s(X), s(Y)) → U7(X, Y, geq_in(X, Y))
U7(X, Y, geq_out(X, Y)) → geq_out(s(X), s(Y))
U5(X, Y, geq_out(X, Y)) → rem_out(X, Y, X)
rem_in(X, Y, R) → U1(X, Y, R, notZero_in(Y))
U1(X, Y, R, notZero_out(Y)) → U2(X, Y, R, sub_in(X, Y, Z))
sub_in(X, 0, X) → sub_out(X, 0, X)
sub_in(s(X), s(Y), Z) → U6(X, Y, Z, sub_in(X, Y, Z))
U6(X, Y, Z, sub_out(X, Y, Z)) → sub_out(s(X), s(Y), Z)
U2(X, Y, R, sub_out(X, Y, Z)) → U3(X, Y, R, rem_in(Z, Y, R))
U3(X, Y, R, rem_out(Z, Y, R)) → rem_out(X, Y, R)
REM_IN(X, Y, X) → U41(X, Y, notZero_in(Y))
REM_IN(X, Y, X) → NOTZERO_IN(Y)
U41(X, Y, notZero_out(Y)) → U51(X, Y, geq_in(X, Y))
U41(X, Y, notZero_out(Y)) → GEQ_IN(X, Y)
GEQ_IN(s(X), s(Y)) → U71(X, Y, geq_in(X, Y))
GEQ_IN(s(X), s(Y)) → GEQ_IN(X, Y)
REM_IN(X, Y, R) → U11(X, Y, R, notZero_in(Y))
REM_IN(X, Y, R) → NOTZERO_IN(Y)
U11(X, Y, R, notZero_out(Y)) → U21(X, Y, R, sub_in(X, Y, Z))
U11(X, Y, R, notZero_out(Y)) → SUB_IN(X, Y, Z)
SUB_IN(s(X), s(Y), Z) → U61(X, Y, Z, sub_in(X, Y, Z))
SUB_IN(s(X), s(Y), Z) → SUB_IN(X, Y, Z)
U21(X, Y, R, sub_out(X, Y, Z)) → U31(X, Y, R, rem_in(Z, Y, R))
U21(X, Y, R, sub_out(X, Y, Z)) → REM_IN(Z, Y, R)
rem_in(X, Y, X) → U4(X, Y, notZero_in(Y))
notZero_in(s(X)) → notZero_out(s(X))
U4(X, Y, notZero_out(Y)) → U5(X, Y, geq_in(X, Y))
geq_in(X, 0) → geq_out(X, 0)
geq_in(s(X), s(Y)) → U7(X, Y, geq_in(X, Y))
U7(X, Y, geq_out(X, Y)) → geq_out(s(X), s(Y))
U5(X, Y, geq_out(X, Y)) → rem_out(X, Y, X)
rem_in(X, Y, R) → U1(X, Y, R, notZero_in(Y))
U1(X, Y, R, notZero_out(Y)) → U2(X, Y, R, sub_in(X, Y, Z))
sub_in(X, 0, X) → sub_out(X, 0, X)
sub_in(s(X), s(Y), Z) → U6(X, Y, Z, sub_in(X, Y, Z))
U6(X, Y, Z, sub_out(X, Y, Z)) → sub_out(s(X), s(Y), Z)
U2(X, Y, R, sub_out(X, Y, Z)) → U3(X, Y, R, rem_in(Z, Y, R))
U3(X, Y, R, rem_out(Z, Y, R)) → rem_out(X, Y, R)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PrologToPiTRSProof
REM_IN(X, Y, X) → U41(X, Y, notZero_in(Y))
REM_IN(X, Y, X) → NOTZERO_IN(Y)
U41(X, Y, notZero_out(Y)) → U51(X, Y, geq_in(X, Y))
U41(X, Y, notZero_out(Y)) → GEQ_IN(X, Y)
GEQ_IN(s(X), s(Y)) → U71(X, Y, geq_in(X, Y))
GEQ_IN(s(X), s(Y)) → GEQ_IN(X, Y)
REM_IN(X, Y, R) → U11(X, Y, R, notZero_in(Y))
REM_IN(X, Y, R) → NOTZERO_IN(Y)
U11(X, Y, R, notZero_out(Y)) → U21(X, Y, R, sub_in(X, Y, Z))
U11(X, Y, R, notZero_out(Y)) → SUB_IN(X, Y, Z)
SUB_IN(s(X), s(Y), Z) → U61(X, Y, Z, sub_in(X, Y, Z))
SUB_IN(s(X), s(Y), Z) → SUB_IN(X, Y, Z)
U21(X, Y, R, sub_out(X, Y, Z)) → U31(X, Y, R, rem_in(Z, Y, R))
U21(X, Y, R, sub_out(X, Y, Z)) → REM_IN(Z, Y, R)
rem_in(X, Y, X) → U4(X, Y, notZero_in(Y))
notZero_in(s(X)) → notZero_out(s(X))
U4(X, Y, notZero_out(Y)) → U5(X, Y, geq_in(X, Y))
geq_in(X, 0) → geq_out(X, 0)
geq_in(s(X), s(Y)) → U7(X, Y, geq_in(X, Y))
U7(X, Y, geq_out(X, Y)) → geq_out(s(X), s(Y))
U5(X, Y, geq_out(X, Y)) → rem_out(X, Y, X)
rem_in(X, Y, R) → U1(X, Y, R, notZero_in(Y))
U1(X, Y, R, notZero_out(Y)) → U2(X, Y, R, sub_in(X, Y, Z))
sub_in(X, 0, X) → sub_out(X, 0, X)
sub_in(s(X), s(Y), Z) → U6(X, Y, Z, sub_in(X, Y, Z))
U6(X, Y, Z, sub_out(X, Y, Z)) → sub_out(s(X), s(Y), Z)
U2(X, Y, R, sub_out(X, Y, Z)) → U3(X, Y, R, rem_in(Z, Y, R))
U3(X, Y, R, rem_out(Z, Y, R)) → rem_out(X, Y, R)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDP
↳ PrologToPiTRSProof
SUB_IN(s(X), s(Y), Z) → SUB_IN(X, Y, Z)
rem_in(X, Y, X) → U4(X, Y, notZero_in(Y))
notZero_in(s(X)) → notZero_out(s(X))
U4(X, Y, notZero_out(Y)) → U5(X, Y, geq_in(X, Y))
geq_in(X, 0) → geq_out(X, 0)
geq_in(s(X), s(Y)) → U7(X, Y, geq_in(X, Y))
U7(X, Y, geq_out(X, Y)) → geq_out(s(X), s(Y))
U5(X, Y, geq_out(X, Y)) → rem_out(X, Y, X)
rem_in(X, Y, R) → U1(X, Y, R, notZero_in(Y))
U1(X, Y, R, notZero_out(Y)) → U2(X, Y, R, sub_in(X, Y, Z))
sub_in(X, 0, X) → sub_out(X, 0, X)
sub_in(s(X), s(Y), Z) → U6(X, Y, Z, sub_in(X, Y, Z))
U6(X, Y, Z, sub_out(X, Y, Z)) → sub_out(s(X), s(Y), Z)
U2(X, Y, R, sub_out(X, Y, Z)) → U3(X, Y, R, rem_in(Z, Y, R))
U3(X, Y, R, rem_out(Z, Y, R)) → rem_out(X, Y, R)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
↳ PiDP
↳ PrologToPiTRSProof
SUB_IN(s(X), s(Y), Z) → SUB_IN(X, Y, Z)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ QDPSizeChangeProof
↳ PiDP
↳ PiDP
↳ PrologToPiTRSProof
SUB_IN(s(X)) → SUB_IN(X)
From the DPs we obtained the following set of size-change graphs:
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PrologToPiTRSProof
GEQ_IN(s(X), s(Y)) → GEQ_IN(X, Y)
rem_in(X, Y, X) → U4(X, Y, notZero_in(Y))
notZero_in(s(X)) → notZero_out(s(X))
U4(X, Y, notZero_out(Y)) → U5(X, Y, geq_in(X, Y))
geq_in(X, 0) → geq_out(X, 0)
geq_in(s(X), s(Y)) → U7(X, Y, geq_in(X, Y))
U7(X, Y, geq_out(X, Y)) → geq_out(s(X), s(Y))
U5(X, Y, geq_out(X, Y)) → rem_out(X, Y, X)
rem_in(X, Y, R) → U1(X, Y, R, notZero_in(Y))
U1(X, Y, R, notZero_out(Y)) → U2(X, Y, R, sub_in(X, Y, Z))
sub_in(X, 0, X) → sub_out(X, 0, X)
sub_in(s(X), s(Y), Z) → U6(X, Y, Z, sub_in(X, Y, Z))
U6(X, Y, Z, sub_out(X, Y, Z)) → sub_out(s(X), s(Y), Z)
U2(X, Y, R, sub_out(X, Y, Z)) → U3(X, Y, R, rem_in(Z, Y, R))
U3(X, Y, R, rem_out(Z, Y, R)) → rem_out(X, Y, R)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
↳ PrologToPiTRSProof
GEQ_IN(s(X), s(Y)) → GEQ_IN(X, Y)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ QDPSizeChangeProof
↳ PiDP
↳ PrologToPiTRSProof
GEQ_IN(s(X)) → GEQ_IN(X)
From the DPs we obtained the following set of size-change graphs:
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PrologToPiTRSProof
U21(X, Y, R, sub_out(X, Y, Z)) → REM_IN(Z, Y, R)
REM_IN(X, Y, R) → U11(X, Y, R, notZero_in(Y))
U11(X, Y, R, notZero_out(Y)) → U21(X, Y, R, sub_in(X, Y, Z))
rem_in(X, Y, X) → U4(X, Y, notZero_in(Y))
notZero_in(s(X)) → notZero_out(s(X))
U4(X, Y, notZero_out(Y)) → U5(X, Y, geq_in(X, Y))
geq_in(X, 0) → geq_out(X, 0)
geq_in(s(X), s(Y)) → U7(X, Y, geq_in(X, Y))
U7(X, Y, geq_out(X, Y)) → geq_out(s(X), s(Y))
U5(X, Y, geq_out(X, Y)) → rem_out(X, Y, X)
rem_in(X, Y, R) → U1(X, Y, R, notZero_in(Y))
U1(X, Y, R, notZero_out(Y)) → U2(X, Y, R, sub_in(X, Y, Z))
sub_in(X, 0, X) → sub_out(X, 0, X)
sub_in(s(X), s(Y), Z) → U6(X, Y, Z, sub_in(X, Y, Z))
U6(X, Y, Z, sub_out(X, Y, Z)) → sub_out(s(X), s(Y), Z)
U2(X, Y, R, sub_out(X, Y, Z)) → U3(X, Y, R, rem_in(Z, Y, R))
U3(X, Y, R, rem_out(Z, Y, R)) → rem_out(X, Y, R)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PrologToPiTRSProof
U21(X, Y, R, sub_out(X, Y, Z)) → REM_IN(Z, Y, R)
REM_IN(X, Y, R) → U11(X, Y, R, notZero_in(Y))
U11(X, Y, R, notZero_out(Y)) → U21(X, Y, R, sub_in(X, Y, Z))
notZero_in(s(X)) → notZero_out(s(X))
sub_in(X, 0, X) → sub_out(X, 0, X)
sub_in(s(X), s(Y), Z) → U6(X, Y, Z, sub_in(X, Y, Z))
U6(X, Y, Z, sub_out(X, Y, Z)) → sub_out(s(X), s(Y), Z)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ RuleRemovalProof
↳ PrologToPiTRSProof
U11(X, R, notZero_out) → U21(R, sub_in(X))
REM_IN(X, R) → U11(X, R, notZero_in)
U21(R, sub_out(Y, Z)) → REM_IN(Z, R)
notZero_in → notZero_out
sub_in(X) → sub_out(0, X)
sub_in(s(X)) → U6(sub_in(X))
U6(sub_out(Y, Z)) → sub_out(s(Y), Z)
notZero_in
sub_in(x0)
U6(x0)
U6(sub_out(Y, Z)) → sub_out(s(Y), Z)
POL(0) = 0
POL(REM_IN(x1, x2)) = 2·x1 + x2
POL(U11(x1, x2, x3)) = 2·x1 + x2 + 2·x3
POL(U21(x1, x2)) = x1 + x2
POL(U6(x1)) = 2 + 2·x1
POL(notZero_in) = 0
POL(notZero_out) = 0
POL(s(x1)) = 1 + 2·x1
POL(sub_in(x1)) = 2·x1
POL(sub_out(x1, x2)) = x1 + 2·x2
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ UsableRulesReductionPairsProof
↳ PrologToPiTRSProof
U11(X, R, notZero_out) → U21(R, sub_in(X))
REM_IN(X, R) → U11(X, R, notZero_in)
U21(R, sub_out(Y, Z)) → REM_IN(Z, R)
notZero_in → notZero_out
sub_in(X) → sub_out(0, X)
sub_in(s(X)) → U6(sub_in(X))
notZero_in
sub_in(x0)
U6(x0)
Used ordering: POLO with Polynomial interpretation [25]:
sub_in(s(X)) → U6(sub_in(X))
POL(0) = 0
POL(REM_IN(x1, x2)) = 1 + x1 + x2
POL(U11(x1, x2, x3)) = x1 + x2 + x3
POL(U21(x1, x2)) = 1 + x1 + x2
POL(U6(x1)) = 2·x1
POL(notZero_in) = 1
POL(notZero_out) = 1
POL(s(x1)) = 2·x1
POL(sub_in(x1)) = x1
POL(sub_out(x1, x2)) = 2·x1 + x2
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ QReductionProof
↳ PrologToPiTRSProof
U11(X, R, notZero_out) → U21(R, sub_in(X))
REM_IN(X, R) → U11(X, R, notZero_in)
U21(R, sub_out(Y, Z)) → REM_IN(Z, R)
notZero_in → notZero_out
sub_in(X) → sub_out(0, X)
notZero_in
sub_in(x0)
U6(x0)
U6(x0)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ PrologToPiTRSProof
U11(X, R, notZero_out) → U21(R, sub_in(X))
REM_IN(X, R) → U11(X, R, notZero_in)
U21(R, sub_out(Y, Z)) → REM_IN(Z, R)
notZero_in → notZero_out
sub_in(X) → sub_out(0, X)
notZero_in
sub_in(x0)
U11(X, R, notZero_out) → U21(R, sub_out(0, X))
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ PrologToPiTRSProof
U11(X, R, notZero_out) → U21(R, sub_out(0, X))
REM_IN(X, R) → U11(X, R, notZero_in)
U21(R, sub_out(Y, Z)) → REM_IN(Z, R)
notZero_in → notZero_out
sub_in(X) → sub_out(0, X)
notZero_in
sub_in(x0)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ PrologToPiTRSProof
U11(X, R, notZero_out) → U21(R, sub_out(0, X))
REM_IN(X, R) → U11(X, R, notZero_in)
U21(R, sub_out(Y, Z)) → REM_IN(Z, R)
notZero_in → notZero_out
notZero_in
sub_in(x0)
sub_in(x0)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ PrologToPiTRSProof
U11(X, R, notZero_out) → U21(R, sub_out(0, X))
REM_IN(X, R) → U11(X, R, notZero_in)
U21(R, sub_out(Y, Z)) → REM_IN(Z, R)
notZero_in → notZero_out
notZero_in
REM_IN(X, R) → U11(X, R, notZero_out)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ PrologToPiTRSProof
U11(X, R, notZero_out) → U21(R, sub_out(0, X))
REM_IN(X, R) → U11(X, R, notZero_out)
U21(R, sub_out(Y, Z)) → REM_IN(Z, R)
notZero_in → notZero_out
notZero_in
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ PrologToPiTRSProof
U11(X, R, notZero_out) → U21(R, sub_out(0, X))
REM_IN(X, R) → U11(X, R, notZero_out)
U21(R, sub_out(Y, Z)) → REM_IN(Z, R)
notZero_in
notZero_in
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ PrologToPiTRSProof
U11(X, R, notZero_out) → U21(R, sub_out(0, X))
REM_IN(X, R) → U11(X, R, notZero_out)
U21(R, sub_out(Y, Z)) → REM_IN(Z, R)
U21(z1, sub_out(0, z0)) → REM_IN(z0, z1)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ NonTerminationProof
↳ PrologToPiTRSProof
U11(X, R, notZero_out) → U21(R, sub_out(0, X))
REM_IN(X, R) → U11(X, R, notZero_out)
U21(z1, sub_out(0, z0)) → REM_IN(z0, z1)
U11(X, R, notZero_out) → U21(R, sub_out(0, X))
REM_IN(X, R) → U11(X, R, notZero_out)
U21(z1, sub_out(0, z0)) → REM_IN(z0, z1)
rem_in(X, Y, X) → U4(X, Y, notZero_in(Y))
notZero_in(s(X)) → notZero_out(s(X))
U4(X, Y, notZero_out(Y)) → U5(X, Y, geq_in(X, Y))
geq_in(X, 0) → geq_out(X, 0)
geq_in(s(X), s(Y)) → U7(X, Y, geq_in(X, Y))
U7(X, Y, geq_out(X, Y)) → geq_out(s(X), s(Y))
U5(X, Y, geq_out(X, Y)) → rem_out(X, Y, X)
rem_in(X, Y, R) → U1(X, Y, R, notZero_in(Y))
U1(X, Y, R, notZero_out(Y)) → U2(X, Y, R, sub_in(X, Y, Z))
sub_in(X, 0, X) → sub_out(X, 0, X)
sub_in(s(X), s(Y), Z) → U6(X, Y, Z, sub_in(X, Y, Z))
U6(X, Y, Z, sub_out(X, Y, Z)) → sub_out(s(X), s(Y), Z)
U2(X, Y, R, sub_out(X, Y, Z)) → U3(X, Y, R, rem_in(Z, Y, R))
U3(X, Y, R, rem_out(Z, Y, R)) → rem_out(X, Y, R)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
rem_in(X, Y, X) → U4(X, Y, notZero_in(Y))
notZero_in(s(X)) → notZero_out(s(X))
U4(X, Y, notZero_out(Y)) → U5(X, Y, geq_in(X, Y))
geq_in(X, 0) → geq_out(X, 0)
geq_in(s(X), s(Y)) → U7(X, Y, geq_in(X, Y))
U7(X, Y, geq_out(X, Y)) → geq_out(s(X), s(Y))
U5(X, Y, geq_out(X, Y)) → rem_out(X, Y, X)
rem_in(X, Y, R) → U1(X, Y, R, notZero_in(Y))
U1(X, Y, R, notZero_out(Y)) → U2(X, Y, R, sub_in(X, Y, Z))
sub_in(X, 0, X) → sub_out(X, 0, X)
sub_in(s(X), s(Y), Z) → U6(X, Y, Z, sub_in(X, Y, Z))
U6(X, Y, Z, sub_out(X, Y, Z)) → sub_out(s(X), s(Y), Z)
U2(X, Y, R, sub_out(X, Y, Z)) → U3(X, Y, R, rem_in(Z, Y, R))
U3(X, Y, R, rem_out(Z, Y, R)) → rem_out(X, Y, R)
REM_IN(X, Y, X) → U41(X, Y, notZero_in(Y))
REM_IN(X, Y, X) → NOTZERO_IN(Y)
U41(X, Y, notZero_out(Y)) → U51(X, Y, geq_in(X, Y))
U41(X, Y, notZero_out(Y)) → GEQ_IN(X, Y)
GEQ_IN(s(X), s(Y)) → U71(X, Y, geq_in(X, Y))
GEQ_IN(s(X), s(Y)) → GEQ_IN(X, Y)
REM_IN(X, Y, R) → U11(X, Y, R, notZero_in(Y))
REM_IN(X, Y, R) → NOTZERO_IN(Y)
U11(X, Y, R, notZero_out(Y)) → U21(X, Y, R, sub_in(X, Y, Z))
U11(X, Y, R, notZero_out(Y)) → SUB_IN(X, Y, Z)
SUB_IN(s(X), s(Y), Z) → U61(X, Y, Z, sub_in(X, Y, Z))
SUB_IN(s(X), s(Y), Z) → SUB_IN(X, Y, Z)
U21(X, Y, R, sub_out(X, Y, Z)) → U31(X, Y, R, rem_in(Z, Y, R))
U21(X, Y, R, sub_out(X, Y, Z)) → REM_IN(Z, Y, R)
rem_in(X, Y, X) → U4(X, Y, notZero_in(Y))
notZero_in(s(X)) → notZero_out(s(X))
U4(X, Y, notZero_out(Y)) → U5(X, Y, geq_in(X, Y))
geq_in(X, 0) → geq_out(X, 0)
geq_in(s(X), s(Y)) → U7(X, Y, geq_in(X, Y))
U7(X, Y, geq_out(X, Y)) → geq_out(s(X), s(Y))
U5(X, Y, geq_out(X, Y)) → rem_out(X, Y, X)
rem_in(X, Y, R) → U1(X, Y, R, notZero_in(Y))
U1(X, Y, R, notZero_out(Y)) → U2(X, Y, R, sub_in(X, Y, Z))
sub_in(X, 0, X) → sub_out(X, 0, X)
sub_in(s(X), s(Y), Z) → U6(X, Y, Z, sub_in(X, Y, Z))
U6(X, Y, Z, sub_out(X, Y, Z)) → sub_out(s(X), s(Y), Z)
U2(X, Y, R, sub_out(X, Y, Z)) → U3(X, Y, R, rem_in(Z, Y, R))
U3(X, Y, R, rem_out(Z, Y, R)) → rem_out(X, Y, R)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
REM_IN(X, Y, X) → U41(X, Y, notZero_in(Y))
REM_IN(X, Y, X) → NOTZERO_IN(Y)
U41(X, Y, notZero_out(Y)) → U51(X, Y, geq_in(X, Y))
U41(X, Y, notZero_out(Y)) → GEQ_IN(X, Y)
GEQ_IN(s(X), s(Y)) → U71(X, Y, geq_in(X, Y))
GEQ_IN(s(X), s(Y)) → GEQ_IN(X, Y)
REM_IN(X, Y, R) → U11(X, Y, R, notZero_in(Y))
REM_IN(X, Y, R) → NOTZERO_IN(Y)
U11(X, Y, R, notZero_out(Y)) → U21(X, Y, R, sub_in(X, Y, Z))
U11(X, Y, R, notZero_out(Y)) → SUB_IN(X, Y, Z)
SUB_IN(s(X), s(Y), Z) → U61(X, Y, Z, sub_in(X, Y, Z))
SUB_IN(s(X), s(Y), Z) → SUB_IN(X, Y, Z)
U21(X, Y, R, sub_out(X, Y, Z)) → U31(X, Y, R, rem_in(Z, Y, R))
U21(X, Y, R, sub_out(X, Y, Z)) → REM_IN(Z, Y, R)
rem_in(X, Y, X) → U4(X, Y, notZero_in(Y))
notZero_in(s(X)) → notZero_out(s(X))
U4(X, Y, notZero_out(Y)) → U5(X, Y, geq_in(X, Y))
geq_in(X, 0) → geq_out(X, 0)
geq_in(s(X), s(Y)) → U7(X, Y, geq_in(X, Y))
U7(X, Y, geq_out(X, Y)) → geq_out(s(X), s(Y))
U5(X, Y, geq_out(X, Y)) → rem_out(X, Y, X)
rem_in(X, Y, R) → U1(X, Y, R, notZero_in(Y))
U1(X, Y, R, notZero_out(Y)) → U2(X, Y, R, sub_in(X, Y, Z))
sub_in(X, 0, X) → sub_out(X, 0, X)
sub_in(s(X), s(Y), Z) → U6(X, Y, Z, sub_in(X, Y, Z))
U6(X, Y, Z, sub_out(X, Y, Z)) → sub_out(s(X), s(Y), Z)
U2(X, Y, R, sub_out(X, Y, Z)) → U3(X, Y, R, rem_in(Z, Y, R))
U3(X, Y, R, rem_out(Z, Y, R)) → rem_out(X, Y, R)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDP
SUB_IN(s(X), s(Y), Z) → SUB_IN(X, Y, Z)
rem_in(X, Y, X) → U4(X, Y, notZero_in(Y))
notZero_in(s(X)) → notZero_out(s(X))
U4(X, Y, notZero_out(Y)) → U5(X, Y, geq_in(X, Y))
geq_in(X, 0) → geq_out(X, 0)
geq_in(s(X), s(Y)) → U7(X, Y, geq_in(X, Y))
U7(X, Y, geq_out(X, Y)) → geq_out(s(X), s(Y))
U5(X, Y, geq_out(X, Y)) → rem_out(X, Y, X)
rem_in(X, Y, R) → U1(X, Y, R, notZero_in(Y))
U1(X, Y, R, notZero_out(Y)) → U2(X, Y, R, sub_in(X, Y, Z))
sub_in(X, 0, X) → sub_out(X, 0, X)
sub_in(s(X), s(Y), Z) → U6(X, Y, Z, sub_in(X, Y, Z))
U6(X, Y, Z, sub_out(X, Y, Z)) → sub_out(s(X), s(Y), Z)
U2(X, Y, R, sub_out(X, Y, Z)) → U3(X, Y, R, rem_in(Z, Y, R))
U3(X, Y, R, rem_out(Z, Y, R)) → rem_out(X, Y, R)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
↳ PiDP
SUB_IN(s(X), s(Y), Z) → SUB_IN(X, Y, Z)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ QDPSizeChangeProof
↳ PiDP
↳ PiDP
SUB_IN(s(X)) → SUB_IN(X)
From the DPs we obtained the following set of size-change graphs:
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
GEQ_IN(s(X), s(Y)) → GEQ_IN(X, Y)
rem_in(X, Y, X) → U4(X, Y, notZero_in(Y))
notZero_in(s(X)) → notZero_out(s(X))
U4(X, Y, notZero_out(Y)) → U5(X, Y, geq_in(X, Y))
geq_in(X, 0) → geq_out(X, 0)
geq_in(s(X), s(Y)) → U7(X, Y, geq_in(X, Y))
U7(X, Y, geq_out(X, Y)) → geq_out(s(X), s(Y))
U5(X, Y, geq_out(X, Y)) → rem_out(X, Y, X)
rem_in(X, Y, R) → U1(X, Y, R, notZero_in(Y))
U1(X, Y, R, notZero_out(Y)) → U2(X, Y, R, sub_in(X, Y, Z))
sub_in(X, 0, X) → sub_out(X, 0, X)
sub_in(s(X), s(Y), Z) → U6(X, Y, Z, sub_in(X, Y, Z))
U6(X, Y, Z, sub_out(X, Y, Z)) → sub_out(s(X), s(Y), Z)
U2(X, Y, R, sub_out(X, Y, Z)) → U3(X, Y, R, rem_in(Z, Y, R))
U3(X, Y, R, rem_out(Z, Y, R)) → rem_out(X, Y, R)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
GEQ_IN(s(X), s(Y)) → GEQ_IN(X, Y)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ QDPSizeChangeProof
↳ PiDP
GEQ_IN(s(X)) → GEQ_IN(X)
From the DPs we obtained the following set of size-change graphs:
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
U21(X, Y, R, sub_out(X, Y, Z)) → REM_IN(Z, Y, R)
REM_IN(X, Y, R) → U11(X, Y, R, notZero_in(Y))
U11(X, Y, R, notZero_out(Y)) → U21(X, Y, R, sub_in(X, Y, Z))
rem_in(X, Y, X) → U4(X, Y, notZero_in(Y))
notZero_in(s(X)) → notZero_out(s(X))
U4(X, Y, notZero_out(Y)) → U5(X, Y, geq_in(X, Y))
geq_in(X, 0) → geq_out(X, 0)
geq_in(s(X), s(Y)) → U7(X, Y, geq_in(X, Y))
U7(X, Y, geq_out(X, Y)) → geq_out(s(X), s(Y))
U5(X, Y, geq_out(X, Y)) → rem_out(X, Y, X)
rem_in(X, Y, R) → U1(X, Y, R, notZero_in(Y))
U1(X, Y, R, notZero_out(Y)) → U2(X, Y, R, sub_in(X, Y, Z))
sub_in(X, 0, X) → sub_out(X, 0, X)
sub_in(s(X), s(Y), Z) → U6(X, Y, Z, sub_in(X, Y, Z))
U6(X, Y, Z, sub_out(X, Y, Z)) → sub_out(s(X), s(Y), Z)
U2(X, Y, R, sub_out(X, Y, Z)) → U3(X, Y, R, rem_in(Z, Y, R))
U3(X, Y, R, rem_out(Z, Y, R)) → rem_out(X, Y, R)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
U21(X, Y, R, sub_out(X, Y, Z)) → REM_IN(Z, Y, R)
REM_IN(X, Y, R) → U11(X, Y, R, notZero_in(Y))
U11(X, Y, R, notZero_out(Y)) → U21(X, Y, R, sub_in(X, Y, Z))
notZero_in(s(X)) → notZero_out(s(X))
sub_in(X, 0, X) → sub_out(X, 0, X)
sub_in(s(X), s(Y), Z) → U6(X, Y, Z, sub_in(X, Y, Z))
U6(X, Y, Z, sub_out(X, Y, Z)) → sub_out(s(X), s(Y), Z)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Rewriting
REM_IN(X, R) → U11(X, R, notZero_in)
U21(X, R, sub_out(X, Y, Z)) → REM_IN(Z, R)
U11(X, R, notZero_out) → U21(X, R, sub_in(X))
notZero_in → notZero_out
sub_in(X) → sub_out(X, 0, X)
sub_in(s(X)) → U6(X, sub_in(X))
U6(X, sub_out(X, Y, Z)) → sub_out(s(X), s(Y), Z)
notZero_in
sub_in(x0)
U6(x0, x1)
REM_IN(X, R) → U11(X, R, notZero_out)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
REM_IN(X, R) → U11(X, R, notZero_out)
U21(X, R, sub_out(X, Y, Z)) → REM_IN(Z, R)
U11(X, R, notZero_out) → U21(X, R, sub_in(X))
notZero_in → notZero_out
sub_in(X) → sub_out(X, 0, X)
sub_in(s(X)) → U6(X, sub_in(X))
U6(X, sub_out(X, Y, Z)) → sub_out(s(X), s(Y), Z)
notZero_in
sub_in(x0)
U6(x0, x1)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
REM_IN(X, R) → U11(X, R, notZero_out)
U21(X, R, sub_out(X, Y, Z)) → REM_IN(Z, R)
U11(X, R, notZero_out) → U21(X, R, sub_in(X))
sub_in(X) → sub_out(X, 0, X)
sub_in(s(X)) → U6(X, sub_in(X))
U6(X, sub_out(X, Y, Z)) → sub_out(s(X), s(Y), Z)
notZero_in
sub_in(x0)
U6(x0, x1)
notZero_in
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
REM_IN(X, R) → U11(X, R, notZero_out)
U21(X, R, sub_out(X, Y, Z)) → REM_IN(Z, R)
U11(X, R, notZero_out) → U21(X, R, sub_in(X))
sub_in(X) → sub_out(X, 0, X)
sub_in(s(X)) → U6(X, sub_in(X))
U6(X, sub_out(X, Y, Z)) → sub_out(s(X), s(Y), Z)
sub_in(x0)
U6(x0, x1)
U11(s(x0), y1, notZero_out) → U21(s(x0), y1, U6(x0, sub_in(x0)))
U11(x0, y1, notZero_out) → U21(x0, y1, sub_out(x0, 0, x0))
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Instantiation
U11(x0, y1, notZero_out) → U21(x0, y1, sub_out(x0, 0, x0))
REM_IN(X, R) → U11(X, R, notZero_out)
U21(X, R, sub_out(X, Y, Z)) → REM_IN(Z, R)
U11(s(x0), y1, notZero_out) → U21(s(x0), y1, U6(x0, sub_in(x0)))
sub_in(X) → sub_out(X, 0, X)
sub_in(s(X)) → U6(X, sub_in(X))
U6(X, sub_out(X, Y, Z)) → sub_out(s(X), s(Y), Z)
sub_in(x0)
U6(x0, x1)
U21(s(z0), z1, sub_out(s(z0), x2, x3)) → REM_IN(x3, z1)
U21(z0, z1, sub_out(z0, 0, z0)) → REM_IN(z0, z1)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Instantiation
↳ QDP
↳ QDPOrderProof
U11(x0, y1, notZero_out) → U21(x0, y1, sub_out(x0, 0, x0))
U21(s(z0), z1, sub_out(s(z0), x2, x3)) → REM_IN(x3, z1)
U21(z0, z1, sub_out(z0, 0, z0)) → REM_IN(z0, z1)
REM_IN(X, R) → U11(X, R, notZero_out)
U11(s(x0), y1, notZero_out) → U21(s(x0), y1, U6(x0, sub_in(x0)))
sub_in(X) → sub_out(X, 0, X)
sub_in(s(X)) → U6(X, sub_in(X))
U6(X, sub_out(X, Y, Z)) → sub_out(s(X), s(Y), Z)
sub_in(x0)
U6(x0, x1)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
U11(s(x0), y1, notZero_out) → U21(s(x0), y1, U6(x0, sub_in(x0)))
Used ordering: Combined order from the following AFS and order.
U11(x0, y1, notZero_out) → U21(x0, y1, sub_out(x0, 0, x0))
U21(s(z0), z1, sub_out(s(z0), x2, x3)) → REM_IN(x3, z1)
U21(z0, z1, sub_out(z0, 0, z0)) → REM_IN(z0, z1)
REM_IN(X, R) → U11(X, R, notZero_out)
0 > [U1^12, U2^12, REMIN2] > notZeroout > subin1
0 > [U1^12, U2^12, REMIN2] > s1 > U62 > subin1
U62: [1,2]
U1^12: multiset
s1: multiset
0: multiset
U2^12: multiset
subin1: multiset
REMIN2: multiset
notZeroout: multiset
sub_in(s(X)) → U6(X, sub_in(X))
sub_in(X) → sub_out(X, 0, X)
U6(X, sub_out(X, Y, Z)) → sub_out(s(X), s(Y), Z)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Instantiation
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ UsableRulesProof
U11(x0, y1, notZero_out) → U21(x0, y1, sub_out(x0, 0, x0))
U21(s(z0), z1, sub_out(s(z0), x2, x3)) → REM_IN(x3, z1)
REM_IN(X, R) → U11(X, R, notZero_out)
U21(z0, z1, sub_out(z0, 0, z0)) → REM_IN(z0, z1)
sub_in(X) → sub_out(X, 0, X)
sub_in(s(X)) → U6(X, sub_in(X))
U6(X, sub_out(X, Y, Z)) → sub_out(s(X), s(Y), Z)
sub_in(x0)
U6(x0, x1)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Instantiation
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
U11(x0, y1, notZero_out) → U21(x0, y1, sub_out(x0, 0, x0))
U21(s(z0), z1, sub_out(s(z0), x2, x3)) → REM_IN(x3, z1)
REM_IN(X, R) → U11(X, R, notZero_out)
U21(z0, z1, sub_out(z0, 0, z0)) → REM_IN(z0, z1)
sub_in(x0)
U6(x0, x1)
sub_in(x0)
U6(x0, x1)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Instantiation
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
U11(x0, y1, notZero_out) → U21(x0, y1, sub_out(x0, 0, x0))
U21(s(z0), z1, sub_out(s(z0), x2, x3)) → REM_IN(x3, z1)
U21(z0, z1, sub_out(z0, 0, z0)) → REM_IN(z0, z1)
REM_IN(X, R) → U11(X, R, notZero_out)
U21(s(x0), z1, sub_out(s(x0), 0, s(x0))) → REM_IN(s(x0), z1)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Instantiation
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ NonTerminationProof
U21(s(x0), z1, sub_out(s(x0), 0, s(x0))) → REM_IN(s(x0), z1)
U11(x0, y1, notZero_out) → U21(x0, y1, sub_out(x0, 0, x0))
REM_IN(X, R) → U11(X, R, notZero_out)
U21(z0, z1, sub_out(z0, 0, z0)) → REM_IN(z0, z1)
U21(s(x0), z1, sub_out(s(x0), 0, s(x0))) → REM_IN(s(x0), z1)
U11(x0, y1, notZero_out) → U21(x0, y1, sub_out(x0, 0, x0))
REM_IN(X, R) → U11(X, R, notZero_out)
U21(z0, z1, sub_out(z0, 0, z0)) → REM_IN(z0, z1)